A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A). f  f = f 

latex

Definitions	filter(P;l), b, deq-member(eq;x;L), EqDecider(T), x:A. B(x), x. t(x), x(s), t  T, f  g, f(x)?z, x  dom(f), f(x), a:A fp B(a), A, False, P  Q, xL. P(x), b, P  Q, P & Q, P  Q, Prop, (x  l), if b t else f fi, Unit, , strong-subtype(A;B)
Lemmas	list-set-type, strong-subtype-self, strong-subtype-set3, strong-subtype-deq-subtype, bool wf, eqff to assert, eqtt to assert, ifthenelse wf, append nil sq, l member wf, not wf, assert wf, assert-deq-member, not functionality wrt iff, assert of bnot, iff transitivity, deq-member wf, bnot wf, filter is nil, fpf wf, deq wf